Lambda the Ultimate

The day of the beast has passed without any noticeable effect; Bill Gates has announced his retirement and the Microsoft stock actually goes up. The coast  finally seems safe for another post on the Lang .NET symposium!

Registration for this heavily debated event is now open. I believe that we have a very interesting set of non-Microsoft invited speakers including Gilad Bracha from Sun, William Cook from UT Austin, John Gough from QUT, Miguel de Icaza from Novel, and Shriram Krishnamurthi from Brown; Microsoft folks including Mike Barnett, Gary Flake, Jim Hugunin, Polita Paulus, Don Syme, and Paul Vick; and a fine line-up of submitted papers.

Hope to see you all in Redmond this August!

Graham Hutton and Joel Wright discuss the semantics of interrupts.

Interrupts are important for writing robust, modular programs, but are traditionally viewed as being difficult from a semantic perspective. In this article we present a simple, formally justified, semantics for interrupts.

Although I didn't get into the details of the article (though it will probably interest the more astute LtU readers), what got me interested in the article was the correlation drawn between exceptions and interrupts:

An important concern in modern programming is exceptions, events that cause computations to terminate in non-standard ways. There are two basic kinds of exceptions: those that arise from inside a computation itself, such as a division by zero, and those that arise from outside a computation, such as a timeout. The former are termed synchronous exceptions, because they can only arise at specific points; for example, division by zero can only occur when performing a division. Dually, the latter are termed asynchronous exceptions, because they can potentially arise at any point; for example, a timeout can normally be received at any time. For simplicity, however, we follow the common practice of referring to synchronous exceptions as exceptions, and to asynchronous exceptions as interrupts.

I can't help but think this is related to resumable exceptions that was discussed in the LtU discussion of Common Lisp Exception Handling and Oleg's subsequent implementation in OCaml. That is, aren't interrupts basically a form of asynchronous exceptions that require a resumption mechanism?

Scheme2Js is a Scheme to Javascript compiler distributed under the GPL license. While some effort has been spent on being as close as possible to R5rs, we concentrated mainly on efficiency. Usually Scheme2Js produces Javascript code, that is comparable to hand-written code. In order to achieve this performance, Scheme2Js is not completely R5rs compliant. In particular it lacks support for continuations, exact numbers and it treats tail recursion only partially.

I think Scheme2Js was mentioned in the forum, but I think it might be of more general interest.

A nice touch is that Scheme code can use JavaScript variables and functions, and JavaScript code can use Scheme variables and functions (perhaps not as cool as the Javadot notation of JScheme, but mighty useful anyway).

Scheme2Js is used in HOP.

The Semicolon Wars
Brian Hayes

A laypeople's introduction to the world of programming languages from American Scientist. Includes some history, a high-level overview of different programming paradigms, some guesses at which differences make a difference, some Dijkstra, and some cheap shots at zealots.

Regular LtU readers won't find anything new here, but it's a good article, and it's always nice to see something like this for the general reading public.

It looks like this is going to be an interesting meeting.

The list of speakers is impressive, of course. Alas, not too many presentation titles are available at the moment.

ML Modules and Haskell Type Classes: A Constructive Comparison
Stefan Wehr and Manuel M.T. Chakravarty

Researchers repeatedly observed that the module system of ML and the type class mechanism of Haskell are related. So far, this relationship has not been formally investigated. The work at hand fills this gap by presenting a constructive comparison between ML modules and Haskell type classes; that is, it introduces two formal translations from modules to type classes and vice versa, which enable a thorough comparison of the two concepts.

And the conclusions...

In this work, we demonstrated how ML modules can be translated to Haskell type classes, proved that the translation preserves type correctness, and provided an implementation of the translation. The source language of the translation is a sub-set of Standard ML, the most important feature missing is the ability to define nested structures. The target language is a subset of Haskell 98 extended with multi-parameter type classes and (abstract) associated type synonyms. Abstract associated type synonyms, another contribution of this work, are used to translate abstract types to Haskell. Our practical experience suggests that it is feasible to use the general idea behind the translation for practical programming because some of the overhead introduced by the formal translation is avoided when writing the
Haskell code by hand.

Furthermore, we showed that Haskell type classes can be translated into ML modules by using first-class structures as runtime evidence for type class constraints. We proved that this translation also preserves type correctness and implemented it. The source language of the translation is a subset of Haskell 98, which does not support constructor classes, class methods with constraints, and default definitions for methods. The target language is a subset of Standard ML extended with first-class structures and recursive functors. It is not recommended writing programs in the style of the translation by hand because too much syntactic overhead is introduced by explicit dictionary abstraction and application. However, the translation provides a good starting point for integrating type classes into the ML module system.

Finally, we presented a thorough comparison between ML modules and Haskell type classes, which fills a serious gap in the literature because it is the first comparison between the two concepts that is based on formal translations. The comparison shows that there are also significant differences between modules and type classes.

Sandrine Blazy, Zaynah Dargaye, and Xavier Leroy has written Formal verification of a C-Compiler frontend. Some previous work is already mentioned on LtU here. Abstract:

This paper presents the formal verification of a compiler front-end that translates a subset of the C language into the Cminor intermediate language. The semantics of the source and target languages as well as the translation between them have been written in the speci- fication language of the Coq proof assistant. The proof of observational semantic equivalence between the source and generated code has been machine-checked using Coq. An executable compiler was obtained by automatic extraction of executable Caml code from the Coq specification of the translator, combined with a certified compiler back-end generating PowerPC assembly code from Cminor, described in previous work.

From the press release:

The first of the three steps of the ISO standardization process has been successfully completed. The Working Group in charge of the technical details of the standard, named WG 9 and headed by the convener Mr. James Moore, unanimously approved the Ada 2005 standard on May 1st, 2006.

The press release includes a brief summary of the new features in the new version of the Ada language. Some of these features were mentioned here before.

Inform 7 is a radical revision of Graham Nelson's Inform language for interactive fiction (such as Zork). Whereas Inform 6 and its predecessors were (IMO) very low-level languages with a C-like syntax, Inform 7 is a relational language based on natural language syntax and a semantics based on predicate logic. Nelson describes Inform 7 in his usual erudite style, in:

Graham Nelson. Natural Language, Semantic Analysis and Interactive Fiction. 2005.

The Inform 7 implementation comes with a slick graphical interface (currently available for Mac OS X and Windows), and adopts the metaphor of a book, as indeed do aspects of the language itself.

Well worth taking a look at it.

(Credit to Peter J. Wasilko, from whose forum post on Human Factors I cherry-picked this link.)

Martin Odersky is blogging

Raising Your Abstraction: A Brief History of Scala